Papers with formal verification
Efficient PRM Training Data Synthesis via Formal Verification (2026.findings-acl)
Copied to clipboard
Ryo Kamoi, Yusen Zhang, Nan Zhang, Sarkar Snigdha Sarathi Das, Ranran Haoran Zhang, Wenpeng Yin, Rui Zhang
| Challenge: | Existing approaches for constructing PRM training data rely on human annotation or sampling-based labeling methods that require repeated LLM calls. |
| Approach: | They propose a framework that synthesizes PRM training data by annotating step-level error labels using formal verification tools such as Z3 and Isabelle. |
| Outcome: | The proposed framework synthesizes PRM training data from formal logic and theorem proving tasks without human annotation or additional LLM calls. |
Improving Autoformalization Using Direct Dependency Retrieval (2026.acl-long)
Copied to clipboard
| Challenge: | Existing methods for hallucinate formal dependencies lack scalability and precision to leverage ever-growing public datasets. |
| Approach: | They propose a retrieval-augmented framework based on Direct Dependency Retrieval to generate formal dependencies from natural-language mathematical descriptions and verify their existence via an efficient Suffix Array Check (SAC). |
| Outcome: | The proposed framework outperforms state-of-the-art methods in retrieval precision and recall and can be used to validate formal representations in a public dataset. |
From Informal to Formal – Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs (2025.acl-long)
Copied to clipboard
Jialun Cao, Yaojie Lu, Meiziniu Li, Haoyang Ma, Haokun Li, Mengda He, Cheng Wen, Le Sun, Hongyu Zhang, Shengchao Qin, Shing-Chi Cheung, Cong Tian
| Challenge: | Recent studies in formal mathematical reasoning have shown an unstoppable growth trend. |
| Approach: | They constructed 18k high-quality instruction-response pairs across five mainstream formal specification languages and evaluated them against ten open-sourced LLMs. |
| Outcome: | The proposed model compared instruction-response pairs across five formal specification languages and found that the LLMs were good at writing proof segments when given either the code, or the detailed description of proof steps. |
Theorem Prover as a Judge for Synthetic Data Generation (2025.acl-long)
Copied to clipboard
| Challenge: | Recent studies show that large language models are increasingly capable of tackling mathematical problems. |
| Approach: | They propose an approach that iteratively refines theorem prover formalisation to mitigate errors. |
| Outcome: | The proposed method increases execution rate on the Lean prover from 60% to 87%, while human annotation is replaced with theorem prover feedback. |
Explainable Quantum Program Repair with Verifiable Proof Traces (2026.findings-acl)
Copied to clipboard
| Challenge: | Existing approaches to program repair provide only post-hoc, non-verifiable explanations that are not executable or verifiably. |
| Approach: | They propose a framework that couples repair generation with machine-checkable executable explanations for quantum programs where correctness hinges on subtle semantic properties such as circuit equivalence and fidelity preservation. |
| Outcome: | Experiments on QASMBench with mutation-generated quantum program bugs show that the proposed framework improves both semantic precision and explanation faithfulness over baselines that rely on unconstrained or purely natural-language explanations. |
Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification (2026.findings-acl)
Copied to clipboard
| Challenge: | Existing approaches to training large language models fail to capture deep semantic properties and edge cases. |
| Approach: | They propose a framework that leverages Liquid Haskell proofs for validating equivalence and execution-based counterexamples for inequivalent training. |
| Outcome: | The proposed framework achieves 13.3pp accuracy gain on EquiBench and consistent gains on PySecDB. |